w:World, e:E, t:.
((isnull(a(loc(e);t))))  (t < time(e))  {((first(e))) c (t  time(pred(e)))} 

latex

Definitions	False, P  Q, A, t  T, {T}, x:A. B(x), SQType(T), , -n, n+m, s ~ t, A  B, {x:A| B(x)} , , x:AB(x), b, left + right, P  Q, Dec(P), A c B, a < b, Void, x:A  B(x), b, , a(i;t), isnull(a), P & Q, P  Q, Unit, (i = j), time(e), pred(e), first(e), loc(e), E, World, i  j , #$n, n - m, , s = t
Lemmas	ge wf, nat properties, w-time wf, w-loc wf, w-E wf, world wf, nat wf, not functionality wrt iff, assert of eq int, eq int wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, w-isnull wf, w-a wf, bool wf, bnot wf, not wf, assert wf, false wf, decidable int equal